\begin{tabbing}
$e$ copies $x$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$a$:Atom1\+
\\[0ex](loc($e$) $\parallel$ $a$ \& ($\neg$$x$ when es{-}init(${\it es}$;$e$):vartype(loc($e$);$x$)$\parallel$$a$)
\\[0ex]\& state when $e$$\backslash\backslash$$x$:state@loc($e$)$\backslash\backslash$$x$$\parallel$$a$
\\[0ex]\& $e$ receives $\parallel$ $a$
\\[0ex]\& ($\neg$state after $e$$\backslash\backslash$$x$:state@loc($e$)$\backslash\backslash$$x$$\parallel$$a$))
\-
\end{tabbing}